Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		app(nil,k)	→ k
2:		app(l,nil)	→ l
3:		app(cons(x,l),k)	→ cons(x,app(l,k))
4:		sum(cons(x,nil))	→ cons(x,nil)
5:		sum(cons(x,cons(y,l)))	→ sum(cons(plus(x,y),l))
6:		sum(app(l,cons(x,cons(y,k))))	→ sum(app(l,sum(cons(x,cons(y,k)))))
7:		plus(0,y)	→ y
8:		plus(s(x),y)	→ s(plus(x,y))

There are 7 dependency pairs:


9:		APP(cons(x,l),k)	→ APP(l,k)
10:		SUM(cons(x,cons(y,l)))	→ SUM(cons(plus(x,y),l))
11:		SUM(cons(x,cons(y,l)))	→ PLUS(x,y)
12:		SUM(app(l,cons(x,cons(y,k))))	→ SUM(app(l,sum(cons(x,cons(y,k)))))
13:		SUM(app(l,cons(x,cons(y,k))))	→ APP(l,sum(cons(x,cons(y,k))))
14:		SUM(app(l,cons(x,cons(y,k))))	→ SUM(cons(x,cons(y,k)))
15:		PLUS(s(x),y)	→ PLUS(x,y)

The approximated dependency graph contains 4 SCCs: {9}, {15}, {10} and {12}.

Consider the SCC {9}. There are no usable rules. By taking the AF π with π(APP) = 1 and π(cons) = [2] together with the lexicographic path order with empty precedence, rule 9 is strictly decreasing.

Consider the SCC {15}. There are no usable rules. By taking the AF π with π(PLUS) = 1 together with the lexicographic path order with empty precedence, rule 15 is strictly decreasing.

Consider the SCC {10}. The usable rules are {7,8}. By taking the AF π with π(s) = π(SUM) = 1, π(plus) = 2 and π(cons) = [2] together with the lexicographic path order with empty precedence, the rules in {7,8} are weakly decreasing and rule 10 is strictly decreasing.

Consider the SCC {12}. The constraints could not be solved.

Tyrolean Termination Tool (0.14 seconds) --- May 4, 2006